home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 4 / Apprentice-Release4.iso / Languages / Caml Light 0.7 / examples / kb / kb.ml < prev    next >
Encoding:
Text File  |  1995-06-19  |  4.6 KB  |  139 lines  |  [TEXT/MPS ]
  1. #open "prelude";;
  2. #open "terms";;
  3. #open "equation";;
  4.  
  5. (****************** Critical pairs *********************)
  6.  
  7. (* All (u,sig) such that n/u (&var) unifies with m,
  8.    with principal unifier sig *)
  9. (* super : term -> term -> (num list & subst) list *)
  10. let super m = suprec where rec suprec = function
  11.     Term(_,sons) as n ->
  12.       let collate (pairs,n) son =
  13.        (pairs @ map (fun (u,sig) -> (n::u,sig)) (suprec son), n+1) in
  14.       let insides = fst (it_list collate ([],1) sons) in
  15.         begin try
  16.           ([], unify(m,n)) :: insides
  17.         with Failure _ ->
  18.           insides
  19.         end
  20.   | _ -> []
  21. ;;
  22.  
  23. (* Ex :
  24. let (m,_) = <<F(A,B)>> 
  25. and (n,_) = <<H(F(A,x),F(x,y))>> in super m n;;
  26. ==> [[1],[2,Term ("B",[])];                      x <- B
  27.      [2],[2,Term ("A",[]); 1,Term ("B",[])]]     x <- A  y <- B
  28. *)
  29.  
  30. (* All (u,sig), u&[], such that n/u unifies with m *)
  31. (* super_strict : term -> term -> (num list & subst) list *)
  32. let super_strict m = function
  33.       Term(_,sons) ->
  34.         let collate (pairs,n) son =
  35.           (pairs @ map (fun (u,sig) -> (n::u,sig)) (super m son), n+1) in
  36.         fst (it_list collate ([],1) sons)
  37.     | _ -> []
  38. ;;
  39.  
  40. (* Critical pairs of l1=r1 with l2=r2 *)
  41. (* critical_pairs : term_pair -> term_pair -> term_pair list *)
  42. let critical_pairs (l1,r1) (l2,r2) =
  43.   let mk_pair (u,sig) =
  44.      substitute sig (replace l2 u r1), substitute sig r2 in
  45.   map mk_pair (super l1 l2);;
  46.  
  47. (* Strict critical pairs of l1=r1 with l2=r2 *)
  48. (* strict_critical_pairs : term_pair -> term_pair -> term_pair list *)
  49. let strict_critical_pairs (l1,r1) (l2,r2) =
  50.   let mk_pair (u,sig) =
  51.     substitute sig (replace l2 u r1), substitute sig r2 in
  52.   map mk_pair (super_strict l1 l2)
  53. ;;
  54.  
  55. (* All critical pairs of eq1 with eq2 *)
  56. let mutual_critical_pairs eq1 eq2 =
  57.   (strict_critical_pairs eq1 eq2) @ (critical_pairs eq2 eq1);;
  58.  
  59. (* Renaming of variables *)
  60.  
  61. let rename n (t1,t2) =
  62.   let rec ren_rec = function
  63.     Var k -> Var(k+n)
  64.   | Term(op,sons) -> Term(op, map ren_rec sons) in
  65.   (ren_rec t1, ren_rec t2)
  66. ;;
  67.  
  68. (************************ Completion ******************************)
  69.  
  70. let deletion_message (k,_) =
  71.   print_string "Rule ";print_int k; message " deleted"
  72. ;;
  73.  
  74. (* Generate failure message *)
  75. let non_orientable (m,n) =
  76.     pretty_term m; print_string " = "; pretty_term n; print_newline()
  77. ;;
  78.  
  79. (* Improved Knuth-Bendix completion procedure *)
  80.  
  81. let kb_completion greater = kbrec where rec kbrec rnum rules =
  82.   let normal_form = mrewrite_all rules
  83.   and get_rule k = assoc k rules in process
  84.   where rec process failures = processf
  85.   where rec processf (k,l) =
  86.    (processkl where rec processkl eqs =
  87.      match eqs with
  88.      [] ->
  89.       if k<l then next_criticals (k+1,l) else
  90.       if l<rnum then next_criticals (1,l+1) else
  91.        (match failures with
  92.           [] -> rules (* successful completion *)
  93.         | _  -> message "Non-orientable equations :";
  94.                 do_list non_orientable failures;
  95.                 failwith "kb_completion")
  96.    | (m,n)::eqs ->
  97.       let m' = normal_form m
  98.       and n' = normal_form n
  99.       and enter_rule(left,right) =
  100.         let new_rule = (rnum+1, mk_rule left right) in
  101.           pretty_rule new_rule;
  102.           let left_reducible (_,(_,(l,_))) = reducible left l in
  103.           let redl,irredl = partition left_reducible rules in
  104.             do_list deletion_message redl;
  105.             let irreds = (map right_reduce irredl
  106.                  where right_reduce (m,(_,(l,r))) = 
  107.                        m,mk_rule l (mrewrite_all (new_rule::rules) r))
  108.             and eqs' = map (fun (_,(_,pair)) -> pair) redl in
  109.              kbrec (rnum+1) (new_rule::irreds) [] (k,l) (eqs @ eqs' @ failures)
  110.       in
  111.       if m'=n' then processkl eqs else
  112.       if greater(m',n') then enter_rule(m',n') else
  113.       if greater(n',m') then enter_rule(n',m') else
  114.         process ((m',n')::failures) (k,l) eqs)
  115.   and next_criticals (k,l) =
  116.     try
  117.       let (v,el) = get_rule l in
  118.         if k=l then
  119.           processf (k,l) (strict_critical_pairs el (rename v el))
  120.         else
  121.           try
  122.             let (_,ek) = get_rule k in 
  123.               processf (k,l) (mutual_critical_pairs el (rename v ek))
  124.       with Not_found (*rule k deleted*) -> next_criticals (k+1,l)
  125.     with Not_found (*rule l deleted*) -> next_criticals (1,l+1)
  126. ;;
  127.  
  128. (* complete_rules is assumed locally confluent, and checked Noetherian with
  129.   ordering greater, rules is any list of rules *)
  130.  
  131. let kb_complete greater complete_rules rules =
  132.     let n = check_rules complete_rules
  133.     and eqs = map (fun (_,(_,pair)) -> pair) rules in
  134.     let completed_rules =
  135.       kb_completion greater n complete_rules [] (n,n) eqs in
  136.     message "Canonical set found :";
  137.     pretty_rules (rev completed_rules);()
  138. ;;
  139.